Iof proof for Lemma append overlapping sublists:
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6.
i, j:
. (i < ||L||) 
(j < ||L||) (
(i = j)) ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||
}
{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9.
j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)
}{0..||L||}
11. increasing(f;||L2||+1)
12.
j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
f:{0..||L1 @ [x / L2]||}{0..||L||}
(increasing(f;||L1 @ [x / L2]||)
& (j:{0..||L1 @ [x / L2]||}. (L1 @ [x / L2])[j] = L[(f(j))]))
by ((AssertBY ||[]|| 
0 ((Reduce 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C),(first_nat 3:n)) (first_tok :t) inil_term)))
)
CollapseTHEN (InstConcl [
i.if i 
z ||L1||
Cthen f1(i)
Celse f(i - ||L1||)
Cfi ]))
C1: .....wf..... NILNIL
C1: 14. ||[]|| 0
C1: (i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi ) 
{0..||L1 @ [x / L2]||}{0..||L||}
C2:
C2: 14. ||[]|| 0
C2: increasing(i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi ;||L1 @ [x / L2]||)
C2: & (j:{0..||L1 @ [x / L2]||}.
C2: & ((L1 @ [x / L2])[j] = L[((i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi )(j))])
C3: .....wf..... NILNIL
C3: 14. ||[]|| 0
C3: 15. f2 : {0..||L1 @ [x / L2]||}{0..||L||}
C3: (increasing(f2;||L1 @ [x / L2]||)
C3: (& (j:{0..||L1 @ [x / L2]||}. (L1 @ [x / L2])[j] = L[(f2(j))]))
C3: 
C.